$\forall$$A$:es\_realizer\{i:l\}, $i$:Id.
\\[0ex]($\neg$($\uparrow$R{-}has{-}loc($A$; $i$))) $\Rightarrow$ (R{-}ds($A$; $i$) = fpf{-}empty $\in$ fpf(Id; $x$.Type))